Nuprl Lemma : sys-cmds_wf
11,40
postcript
pdf
Cmd
:Type,
c
:chain_sys(
Cmd
). sys-cmds(
c
)
(
Cmd
List)
latex
Definitions
t
T
,
type
List
,
[]
,
A
List
,
s
=
t
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
[
car
/
cdr
]
,
x
.
A
(
x
)
,
Id
,
x
,
y
.
t
(
x
;
y
)
,
x
.
t
(
x
)
,
chain_sys_ind(
x
;
cmd
.
input
(
cmd
);
from
,
cmds
.
update
(
from
;
cmds
))
,
Type
,
chain_sys(
Cmd
)
,
sys-cmds(
x
)
Lemmas
chain
sys
wf
,
chain
sys
ind
wf
,
Id
wf
origin
Cmd:Type, c:chain_sys(Cmd). sys-cmds(c) 
(Cmd List) Cmd:Type, c:chain_sys(Cmd). sys-cmds(c) (Cmd List) T
B(x)x:A. B(x)
x.A(x)
x,y. t(x;y)x. t(x)